Search for: All records

Since many Cyber–Physical Systems (CPS) interact with the real world, they are safety- or mission- critical. Temporal specification languages like STL (Signal Temporal Logic) have been developed to capture the properties that built CPS must meet. However, the existing temporal logics/languages do not provide a natural way to express the tolerance with which the timing properties must be met. As a consequence of this, the specified properties may be vague, the ensuing CPS design may end up being over- or under-provisioned, and the validation of whether the built CPS meets the specified CPS properties may turn out to be erroneous. To address these issues, a run-time verification methodology is proposed, that allows users to explicitly specify the tolerance with which timing properties must be met. To ensure the correctness of measurement-based validation of a built CPS, this article: (i) proposes a test to determine if a given measurement system can validate the properties specified in TTL, and (ii) proposes a measurement-based testing methodology to provide one-sided guarantee that the built CPS meets the specified CPS properties. The guarantees are one-sided in the sense that when the measurement-based testing concludes that the properties are met, then they are guaranteed to be met (so not false positive). However, when the measurement-based testing concludes that the properties were not met, then they may have met (there can be false negative). In order to validate our claims, we built a model of flying paster (part of the printing press that swaps in a new roll of paper when the current roll is about to finish) using Arduino Mega 2560 and two Hansen brushed DC motors and specified the timing constraints among the various events in this system, along with the tolerances with which they should be met in TTL. We generated the testing logic and validated that we get no false positive, even though we encounter 4.04% false negative. The rate of false negatives can be reduced to be less than any arbitrary value by using more accurate measurement equipment. 

NOTE: DOI IS available but the nsfpar system rejects it: 10.1007/978-3-030-41131-2_4 This paper describes a component-based concurrent model of computation for reactive systems. The components in this model, featuring ports and hierarchy, are called reactors. The model leverages a semantic notion of time, an event scheduler, and a synchronous-reactive style of communication to achieve determinism. Reactors enable a programming model that ensures determinism, unless explicitly abandoned by the programmer. We show how the coordination of reactors can safely and transparently exploit parallelism, both in shared-memory and distributed systems.